Inference at * 
Iof proof for Lemma p-filter wf:


  T:Type, P:(T), f:(x:T. Dec(P(x))). p-filter(f)  T(T + Top) 

latex

 by ((Unfolds ``all decidable p-filter`` 0) 
CollapseTHEN (Auto)) 

latex

Co.

Definitions	Dec(P), p-filter(f), x.A(x), case b of inl(x) => s(x) | inr(y) => t(y), inl x , inr x , Top, x:A.B(x), Void, P  Q, left + right, A, x:A. B(x), x(s), f(a), x:AB(x), , t  T, Type
Lemmas	top wf, not wf